(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 498
Accept states: [499, 500, 501]
Transitions:
498→499[i_1|0]
498→500[j_1|0]
498→501[p_1|0]
498→498[0_1|0, s_1|0]
498→502[s_1|1]
498→510[s_1|1]
498→520[s_1|1]
498→528[s_1|1]
498→545[s_1|1]
498→504[s_1|2]
498→512[s_1|2]
498→547[s_1|2]
498→506[0_1|2]
498→514[0_1|2]
498→549[i_1|2]
498→536[s_1|2]
498→538[s_1|2]
498→540[j_1|2]
502→503[p_1|1]
503→504[s_1|1]
503→506[0_1|2]
504→505[p_1|1]
505→506[0_1|1]
506→507[s_1|1]
506→509[s_1|2]
506→550[s_1|2]
506→554[s_1|2]
507→508[p_1|1]
508→509[s_1|1]
508→550[s_1|2]
508→554[s_1|2]
509→499[p_1|1]
509→549[p_1|1]
510→511[p_1|1]
511→512[s_1|1]
511→514[0_1|2]
512→513[p_1|1]
513→514[0_1|1]
514→515[s_1|1]
514→519[s_1|2]
514→541[s_1|2]
515→516[s_1|1]
515→518[p_1|2]
516→517[p_1|1]
517→518[p_1|1]
518→519[s_1|1]
518→541[s_1|2]
519→500[p_1|1]
519→540[p_1|1]
520→521[s_1|1]
521→522[s_1|1]
522→523[s_1|1]
523→524[s_1|1]
524→525[s_1|1]
525→526[s_1|1]
526→527[s_1|1]
527→501[0_1|1]
528→529[s_1|1]
528→535[p_1|2]
529→530[s_1|1]
529→534[p_1|2]
530→531[s_1|1]
530→533[p_1|2]
531→532[p_1|1]
532→533[p_1|1]
533→534[p_1|1]
534→535[p_1|1]
535→536[s_1|1]
535→538[s_1|2]
535→540[j_1|2]
536→537[p_1|1]
537→538[s_1|1]
537→540[j_1|2]
538→539[p_1|1]
539→540[j_1|1]
540→541[s_1|1]
541→542[s_1|1]
541→544[s_1|2]
541→550[s_1|2]
541→554[s_1|2]
542→543[p_1|1]
543→544[s_1|1]
543→550[s_1|2]
543→554[s_1|2]
544→499[p_1|1]
544→549[p_1|1]
545→546[p_1|1]
546→547[s_1|1]
546→549[i_1|2]
547→548[p_1|1]
548→549[i_1|1]
549→550[s_1|1]
549→554[s_1|2]
550→551[s_1|1]
550→553[p_1|2]
551→552[p_1|1]
552→553[p_1|1]
553→554[s_1|1]
554→555[s_1|1]
555→556[s_1|1]
556→500[s_1|1]
556→540[s_1|1]